|
In mathematical logic, the De Bruijn notation is a syntax for terms in the λ calculus invented by the Dutch mathematician Nicolaas Govert de Bruijn. It can be seen as a reversal of the usual syntax for the λ calculus where the argument in an application is placed next to its corresponding binder in the function instead of after the latter's body. == Formal definition == Terms () in the De Bruijn notation are either variables (), or have one of two ''wagon'' prefixes. The ''abstractor wagon'', written , corresponds to the usual λ-binder of the λ calculus, and the ''applicator wagon'', written , corresponds to the argument in an application in the λ calculus. : Terms in the traditional syntax can be converted to the De Bruijn notation by defining an inductive function for which: All operations on λ-terms commute with respect to the translation. For example, the usual β-reduction, : in the De Bruijn notation is, predictably, : A feature of this notation is that abstractor and applicator wagons of β-redexes are paired like parentheses. For example, consider the stages in the β-reduction of the term , where the redexes are underlined:〔 The example is from page 384.〕 Thus, if one views the applicator as an open paren (' (') and the abstractor as a close bracket (']'), then the pattern in the above term is '((](]]'. De Bruijn called an applicator and its corresponding abstractor in this interpretation ''partners'', and wagons without partners ''bachelors''. A sequence of wagons, which he called a ''segment'', is ''well balanced'' if all its wagons are partnered.抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「De Bruijn notation」の詳細全文を読む スポンサード リンク
|